We investigates the concept of strong equivalence within the extended framework of Answer Set Programming with constraints. Two groups of rules are considered strongly equivalent if, informally speaking, they have the same meaning in any context. We demonstrate that, under certain assumptions, strong equivalence between rule sets in this extended setting can be precisely characterized by their equivalence in the logic of Here-and-There with constraints. Furthermore, we present a translation from the language of several clingo-based answer set solvers that handle constraints into the language of Here-and-There with constraints. This translation enables us to leverage the logic of Here-and-There to reason about strong equivalence within the context of these solvers. We also explore the computational complexity of determining strong equivalence in this context.

Over the last decades the development of ASP has brought about an expressive modeling language powered by highly performant systems. At the same time, it gets more and more difficult to provide semantic underpinnings capturing the resulting constructs and inferences. This is even more severe when it comes to hybrid ASP languages and systems that are often needed to handle real-world applications. We address this challenge and introduce the concept of abstract and structured theories that allow us to formally elaborate upon their integration with ASP. We then use this concept to make precise the semantic characterization of CLINGO's theory-reasoning framework and establish its correspondence to the logic of Here-and-there with constraints. This provides us with a formal framework in which we can elaborate formal properties of existing hybridizations of CLINGO such as CLINGCON, CLINGOM[DL], and CLINGO[LP].

Answer Set Programming (ASP) has become a popular and quite sophisticated approach to declarative problem solving. This is arguably due to its attractive modeling-grounding-solving workflow that provides an easy approach to problem solving, even for laypersons outside computer science. Unlike this, the high degree of sophistication of the underlying technology makes it increasingly hard for ASP experts to put ideas into practice. For addressing this issue, this tutorial aims at enabling users to build their own ASP-based systems. More precisely, we show how the ASP system CLINGO can be used for extending ASP and for implementing customized special-purpose systems. To this end, we propose two alternatives. We begin with a traditional AI technique and show how meta programming can be used for extending ASP. This is a rather light approach that relies on CLINGO's reification feature to use ASP itself for expressing new functionalities. Unlike this, the major part of this tutorial uses traditional programming (in PYTHON) for manipulating CLINGO via its application programming interface. This approach allows for changing and controlling the entire model-ground-solve workflow of ASP. Central to this is CLINGO's new Application class that allows us to draw on CLINGO's infrastructure by customizing processes similar to the one in CLINGO. For instance, we may engage manipulations to programs' abstract syntax trees, control various forms of multi-shot solving, and set up theory propagators for foreign inferences. Another cross-sectional structure, spanning meta as well as application programming, is CLINGO's intermediate format, ASPIF, that specifies the interface among the underlying grounder and solver. We illustrate the aforementioned concepts and techniques throughout this tutorial by means of examples and several non-trivial case-studies.

Answer set programming is a programming paradigm where a given problem is formalized as a logic program whose answer sets correspond to the solutions to the problem. In this paper, we link answer set programming with another widely applied paradigm, viz.~mixed integer programming. As a theoretical result, we establish translations from non-disjunctive logic programs to linear constraints used in mixed integer programming so that the solutions to the constraints correspond to the answer sets of the programs. These translations create the basis for an extended answer set programming language that includes linear constraints as a primitive and enables more compact encodings of problems. On a practical level, we have implemented a prototype system that computes answer sets using a state-of-the-art mixed integer programming solver. The reported experiments demonstrate the effectiveness of this approach applied to a number of optimization problems and problems with variables ranging over large domains.